COMMENT ⊗   VALID 00005 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	(wipe-out)
C00003 00003	selection: 7 lines
C00005 00004	diagonalisation: 13 lines			***bug?***
C00010 00005	the proof of ramsey's theorem: 11 lines
C00017 ENDMK
C⊗;
(wipe-out)
(get-proofs natset prf ekl sys)                       ;need the natset file
;time: 34s
;selection: 7 lines
;4s

(proof select)

(define select |∀f a.select(f,a)=(if unbound(inverse(f,a,0)) then 0 else 1)|)
(label simpinfo)

(decl stabilize (type: |@funct⊗@set→@set|))
(define stabilize
        |∀f a.stabilize(f,a)=
	      (if unbound(inverse(f,a,0)) then inverse(f,a,0) else inverse(f,a,1))|)
(label simpinfo) 

(trw |select(f,a)=0∨select(f,a)=1| (open select))
;SELECT(F,A)=0∨SELECT(F,A)=1
(label simpinfo)

(trw |stabilize(f,a)⊂a| (open stabilize))
;STABILIZE(F,A)⊂A
(label simpinfo)

(trw |nεstabilize(f,a)⊃f(n)=select(f,a)| (open stabilize select inverse epsilon))
;NεSTABILIZE(F,A)⊃F(N)=SELECT(F,A)
(label stabselprop)

(trw |(∀n.f(n)=0∨f(n)=1)∧unbound(a)⊃unbound(stabilize(f,a))|
     (open stabilize) (use split_unbound))
;(∀N.F(N)=0∨F(N)=1)∧UNBOUND(A)⊃UNBOUND(STABILIZE(F,A))
(label splitprop)
;diagonalisation: 13 lines			***bug?***
;11s
(proof diagonalize)

(assume |∀n.seq(n')⊂seq(n)∧unbound(seq(n))|)
(label diagonal_assumption)
 
(ue (rel |λn m.seq(m)⊂seq(n)|) transitive_induction
    (use diagonal_assumption)
    (part 1 (open transitive inclusion)))
;∀N M.N<M⊃SEQ(M)⊂SEQ(N)
;deps: (DIAGONAL_ASSUMPTION)
(label diagonal_step1)

(define diagset |∀n.diagset(n)≡(∀m.mεdiagset∩segm(n)⊃nεseq(m))| 
	(use course_of_values_definition))

(trw |∀n m.n<m∧diagset(n)∧diagset(m)⊃mεseq(n)|
     (open epsilon segm intersection diagset))
;∀N M.N<M∧DIAGSET(N)∧DIAGSET(M)⊃MεSEQ(N)
(label diagonal_step2)

(assume |¬unbound(diagset)|)
(label assume_not)

(rw assume_not (use boundfact mode: always) (open inclusion epsilon segm))
;∀N.DIAGSET(N)⊃N<BOUND(DIAGSET)
;deps: (ASSUME_NOT)
(label diagset_bound)

;find a counter example
(decl ctr (sort: natnum))
(define ctr |ctrεseq(bound(diagset))∧¬(ctrεsegm(bound(diagset)))|
	(der diagonal_assumption inclusiondef unboundef epsilondef))
(label counterexample)

(trw |∀m.diagset(m)⊃(seq(m))(ctr)| 
     (der diagset_bound diagonal_step1 inclusiondef epsilondef counterexample))
;∀M.DIAGSET(M)⊃(SEQ(M))(CTR)
;deps: (DIAGONAL_ASSUMPTION ASSUME_NOT)

(trw |diagset(ctr)| (open diagset epsilon intersection) (use *))
;DIAGSET(CTR)
;deps: (DIAGONAL_ASSUMPTION ASSUME_NOT)
 
(rw counterexample (open epsilon segm))
;(SEQ(BOUND(DIAGSET)))(CTR)∧¬CTR<BOUND(DIAGSET)
;deps: (DIAGONAL_ASSUMPTION)

(tci (assume_not) false (der -1 -2 diagset_bound))
;UNBOUND(DIAGSET)
;deps: (DIAGONAL_ASSUMPTION)

(tci (diagonal_assumption) |∃a.unbound(a)∧∀n m.n<m∧a(n)∧a(m)⊃mεseq(n)|
     (der * diagonal_step2))
;(∀N.SEQ(N')⊂SEQ(N)∧UNBOUND(SEQ(N)))⊃
;(∃A.UNBOUND(A)∧(∀N M.N<M∧A(N)∧A(M)⊃MεSEQ(N)))
(label diagonalprop)
;the proof of ramsey's theorem: 11 lines
;19s

(proof ramsey)

(assume |∀n m.hf(n,m)=0∨hf(n,m)=1|)
(label assumption)

;this is the first stabilisation
(define stab1 
   |stab1(0)=stabilize(λxv.hf(0,xv),univ)∧
    (∀n.stab1(n')=stabilize(λxv.hf(n',xv),stab1(n)))|
   (use inductive_set_definition))
 
;establish two facts for diagonalisation

(trw |∀n.stab1(n')⊂stab1(n)| (open stab1))
;∀N.STAB1(N')⊂STAB1(N)

(ue (a |λxv.unbound(stab1(xv))|) proof_by_induction
    (use splitprop assumption) (open stab1))
;∀N.UNBOUND(STAB1(N))
;deps: (ASSUMPTION)

;now diagonalize
(define hom1 |unbound(hom1)∧(∀n m.n<m∧hom1(n)∧hom1(m)⊃mεstab1(n))|
	(use -1 -2) (use diagonalprop ue: ((seq . stab1))))
;deps: (ASSUMPTION)
(label hom1prop)

;define the value of h on diagonal sets
(define stabf |stabf(0)=select(λxv.hf(0,xv),univ)∧
	       ∀n.stabf(n')=select(λxv.hf(n',xv),stab1(n))|
	(use inductive_definition))

;verify the value
(ue (a  |λn.((∀m.mεstab1(n)⊃hf(n,m)=stabf(n))∧(stabf(n)=0∨stabf(n)=1))|)
    proof_by_induction
    (open stabf stab1) (use stabselprop ue: ((f.|λxv.hf(n,xv)|)) ))
;∀N.(∀M.MεSTAB1(N)⊃HF(N,M)=STABF(N))∧(STABF(N)=0∨STABF(N)=1)
(label stabfprop)

;define the ultimate stable set
(decl hom (type: |@set|))
(define hom |hom=stabilize(stabf,hom1)|)
      
;verify the properties of the stable set
(trw |unbound(hom)∧∀n m.(n<m∧hom(n)∧hom(m)⊃hf(n,m)=select(stabf,hom1))|
     (part 1 (open hom) (use hom1prop stabfprop splitprop))
     (part 2 (open select hom hom1 stabilize inverse) (use stabfprop hom1prop)))
;UNBOUND(HOM)∧(∀N M.N<M∧HOM(N)∧HOM(M)⊃HF(N,M)=SELECT(STABF,HOM1))
;deps: (ASSUMPTION)

;now wrap it all up
(tci (assumption) |∃hm v.unbound(hm)∧(∀n m.n<m∧hm(n)∧hm(m)⊃hf(n,m)=v)| (use *))
;(∀N M.HF(N,M)=0∨HF(N,M)=1)⊃(∃HM V.UNBOUND(HM)∧(∀N M.N<M∧HM(N)∧HM(M)⊃HF(N,M)=V))